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 ) )

A2: 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 that
A3: zz divides x and
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 ex zz9 being Element of F st zz9 * zz = 1_ F by VECTSP_1:def 20;
hence zz divides 1_ F by Def1; :: thesis: verum

end;

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

assume zz divides x ; :: thesis: zz divides 1_ F
then ex d being Element of F st zz * d = x by Def1;
hence zz divides 1_ F by A1, A4, VECTSP_1:39; :: thesis: verum

end;

end;

end;

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

end;

y = (1_ F) * y by VECTSP_1:def 19;
then A5: 1_ F divides y by Def1;
x = (1_ F) * x by VECTSP_1:def 19;
then 1_ F divides x by Def1;
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 A5, A2; :: thesis: verum

end;

case A6: 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 A7: 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 A6, A7; :: thesis: verum

end;

case A8: 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 A9: 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 A8, A9; :: 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