let F be non empty right_complementable almost_left_invertible commutative right-distributive left-distributive well-unital left_unital add-associative right_zeroed doubleLoopStr ; :: thesis: F is gcd-like
let x, y be Element of F; :: according to GCD_1:def 11 :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )

now

per cases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;

case A1: ( x <> 0. F & y <> 0. F ) ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )

x = (1_ F) * x by VECTSP_1:def 19;
then A2: 1_ F divides x by Def1;
y = (1_ F) * y by VECTSP_1:def 19;
then A3: 1_ F divides y by Def1;
for zz being Element of F st zz divides x & zz divides y holds
zz divides 1_ F

proof

let zz be Element of F; :: thesis: ( zz divides x & zz divides y implies zz divides 1_ F )
assume A4: ( zz divides x & zz divides y ) ; :: thesis: zz divides 1_ F

now

per cases ( zz <> 0. F or zz = 0. F ) ;

case zz <> 0. F ; :: thesis: zz divides 1_ F

then consider zz' being Element of F such that
A5: zz' * zz = 1_ F by VECTSP_1:def 20;
thus zz divides 1_ F by A5, Def1; :: thesis: verum

end;

case A6: zz = 0. F ; :: thesis: ( zz divides x implies zz divides 1_ F )

assume zz divides x ; :: thesis: zz divides 1_ F
then consider d being Element of F such that
A7: zz * d = x by Def1;
thus zz divides 1_ F by A1, A6, A7, VECTSP_1:39; :: thesis: verum

end;

end;

end;

hence zz divides 1_ F by A4; :: thesis: verum

end;

hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A2, A3; :: thesis: verum

end;

case A8: x = 0. F ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )

y * (0. F) = 0. F by VECTSP_1:36;
then A9: y divides 0. F by Def1;
for z being Element of F st z divides 0. F & z divides y holds
z divides y ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A8, A9; :: thesis: verum

end;

case A10: y = 0. F ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )

x * (0. F) = 0. F by VECTSP_1:36;
then A11: x divides 0. F by Def1;
for z being Element of F st z divides x & z divides 0. F holds
z divides x ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A10, A11; :: thesis: verum

end;

end;

end;

hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ; :: thesis: verum